Nuprl Lemma : es-is-interface-p-first
11,40
postcript
pdf
es
:ES,
A
:Type,
Ias
:(AbsInterface(
A
) List),
e
:E. (
(
e
p-first(
Ias
)))
(
I
Ias
.
(
e
I
))
latex
Definitions
E
,
x
:
A
.
B
(
x
)
,
Top
,
left
+
right
,
x
:
A
B
(
x
)
,
type
List
,
Type
,
ES
,
e
X
,
AbsInterface(
A
)
Lemmas
can-apply-p-first
origin
es:ES, A:Type, Ias:(AbsInterface(A) List), e:E. (
(e 
p-first(Ias))) 
(
IIas.(e I)) es:ES, A:Type, Ias:(AbsInterface(A) List), e:E. ((e p-first(Ias))) (IIas.(e I)) x:A. B(x)
B(x) X